A:Type, P:((A List)Prop). strong_safety(A;x.P(x))  safety(A;x.P(x)) 

latex

Definitions	P  Q, x:A. B(x), x:A. B(x), l1  l2, L1  L2, {T}, t  T, Prop, x(s), safety(A;tr.P(tr)), strong_safety(T;tr.P(tr))
Lemmas	iseg wf, sublist wf, sublist weakening, interleaving sublist, sublist iseg